/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.*;
import java.util.*;

import common.*;



public class Network extends Net{

    /**
     * 
     */
    private static final long serialVersionUID = -4084943285441767994L;

    public Network()
    {

        //do nothing

    }

    public Network(String name) throws IOException
    {
        this(name, false, false);
    }

    public Network(String name, Boolean use_mpls) throws IOException
    {
        this(name, use_mpls, false);
    }

    public Network(String name, Boolean use_mpls, Boolean use_v6) throws IOException
    {
        this.name = name;

        boxes = new HashMap<String, Box>();

        String foldername2 = "i2old/";
        //String [] devicenames = {"atla","clev","chic","hous","kans","losa","newy32aoa","salt","seat","wash"};
        String [] devicenames = {"atla","chic","hous","kans","losa","newy32aoa","salt","seat","wash"};
        edgerouters = new ArrayList<String>(Arrays.asList(devicenames));
        BuildNetwork.set_al2s(false);

        bddengine = new BDDACLWrapper();
        Box.setBDDWrapper(bddengine);
        MPLSTable.set_bdd_engine(bddengine);
        IPinIP.set_bdd_engine(bddengine);

        readTopology(foldername2 + "i2_old_topology");

        for( int i = 0; i < devicenames.length; i ++)
        {
            Device d = BuildNetwork.parseDevice(devicenames[i], foldername2 + devicenames[i] + "ap");
            if(use_mpls)
            {
                d.read_mpls_table(foldername2 + devicenames[i] + "mpls");
                //System.out.println(d.mpls_table.num_rules() + " " + d.mpls_table.num_bdd_nodes());
            }
            if(use_v6)
            {
                Device.has_v6 = true;
                BuildNetwork.readParsed6(d, new File(foldername2 + devicenames[i] + "v6"));
            }else
            {
                Device.has_v6 = false;
            }

            //System.out.println(d.name);
            boxes.put(d.name, d);
        }


        for(Box d : boxes.values())
        {
            //long t1 = System.nanoTime();

            ((Device) d).computeFWBDDs();

            //long t2 = System.nanoTime();
            //System.out.println(d.name + " computing bdds takes " + (t2 - t1) + "ns");
        }


        if(use_v6)
        {
            for(Box d : boxes.values())
            {
                ((Device)d).computeFWBDDs6();
                System.out.println(((Device)d).fws6.size() + " " + bddengine.getNodeSize(((Device)d).fwbdds6.values()));
            }
        }

        setactiveports();


        for(String r : edgerouters)
        {
            Device d = (Device) boxes.get(r);
            Set<String> usedports = d.fwbdds.keySet();
            for(String port : usedports)
            {
                PositionTuple pt = new PositionTuple(d.getName(), port);
                if((!topology.containsKey(pt)) && d.find_nat_subnet(port))
                {
                    System.out.println(d.getName()+": find own prefix");
                    break;
                }
            }

        }

        // save to file
        //PrintWriter pw = new PrintWriter(new File(name+"_nat"));
        //for(String r : edgerouters)
        //{
        //      Device d = (Device) boxes.get(r);
        //      pw.println(d.name+" " + d.nat_addr);
        //}
        //pw.close();

        int num_links = 0;
        for(PositionTuple port : topology.keySet())
        {
            num_links += topology.get(port).size();
        }
        System.out.println(num_links + "/2 links.");

    }

    public void readTopology(String filename) throws FileNotFoundException
    {
        topology = new HashMap<PositionTuple, HashSet<PositionTuple>>();

        Scanner one_line = new Scanner (new File(filename));
        one_line.useDelimiter("\n");
        while(one_line.hasNext())
        {
            String line_str = one_line.next();
            //System.out.println(line_str);
            if (line_str.length() > 0)
            {
                String[] tokens = line_str.split(" ");
                addTopology(tokens[0], tokens[1], tokens[2], tokens[3]);
            }
        }

        one_line.close();
    }



    public void add_nat_each_edge(int nat_num)
    {
        int cnt = 0;
        for(int j = 0; j < nat_num; j ++)
        {
            for(int i = 0; i < edgerouters.size(); i++)
            {
                Device d = (Device) boxes.get(edgerouters.get(i));
                PositionTuple pt_r = d.add_nat();
                int old_pkt = d.fwbdds.get(pt_r.getPortName());
                bddengine.ref(old_pkt);

                NATBox nat = new NATBox("nat"+cnt);
                //nat.add_entry_out(BDDACLWrapper.BDDTrue, bddengine.get_field_bdd(Fields.dst_ip), 
                //            bddengine.encodeDstIPPrefix(12345678L, 32));
                nat.add_entry_out(old_pkt, bddengine.get_field_bdd(Fields.dst_ip), 
                        bddengine.encodeDstIPPrefix(12345678L, 32));

                PositionTuple pt_nat = new PositionTuple(nat.getName(), NATBox.port_out);
                addTopology(pt_r, pt_nat);
                addBox(nat);

                cnt ++;
            }
        }
    }

    public class MPLSPathUnit{
        String device_name;
        int in_label;
        MPLSTable.table_entry_bdd table_entry;
        public MPLSPathUnit(String dname, int in_l, MPLSTable.table_entry_bdd entry)
        {
            device_name = dname;
            in_label = in_l;
            table_entry = entry;
        }

        public boolean connect_to(MPLSPathUnit nextUnit)
        {
            String port = table_entry.ports.iterator().next();
            PositionTuple pt = new PositionTuple(device_name, port);
            if(topology.containsKey(pt))
            {
                HashSet<PositionTuple> pts = topology.get(pt);
                for(PositionTuple nextpt : pts)
                {
                    if(nextpt.getDeviceName().equals(nextUnit.device_name))
                    {
                        if(table_entry.out_label_bdd == nextUnit.in_label)
                        {
                            return true;
                        }
                    }
                }
            }

            return false;
        }

        public String toString()
        {
            return device_name + " " + in_label;
        }
    }

    public ArrayList<ArrayList<MPLSPathUnit>> extract_mpls_path()
    {
        ArrayList<ArrayList<MPLSPathUnit>> paths = new ArrayList<ArrayList<MPLSPathUnit>>();

        for(String d : boxes.keySet())
        {
            Device device = (Device) boxes.get(d);
            for(Integer in_label : device.mpls_table.swap_table_bdd.keySet())
            {
                MPLSPathUnit mpu = new MPLSPathUnit(d, in_label, device.mpls_table.swap_table_bdd.get(in_label));
                ArrayList<MPLSPathUnit> one_path = new ArrayList<MPLSPathUnit>();
                one_path.add(mpu);
                paths.add(one_path);
            }
        }
        System.out.println(paths.size() + " MPLS Path Units");
        boolean can_extend = true;
        while(can_extend)
        {
            can_extend = false;
            ArrayList<MPLSPathUnit> path_i = null;
            ArrayList<MPLSPathUnit> path_j = null;
            int j_index = -1;
            for(int i = 0; i < paths.size(); i ++)
            {
                path_i = paths.get(i);
                for(int j = 0; j < paths.size(); j ++)
                {
                    path_j = paths.get(j);
                    if(path_i.get(path_i.size()-1).connect_to(path_j.get(0)))
                    {
                        j_index = j;
                        can_extend = true;
                        break;
                    }
                }
                if(can_extend)
                {
                    break;
                }
            }
            if(can_extend)
            {
                path_i.addAll(path_j);
                paths.remove(j_index);
                //System.out.println(j_index);
            }
        }
        System.out.println(paths.size() + " MPLS paths");
        int max_len = 1;
        for(ArrayList<MPLSPathUnit> path : paths)
        {
            if(max_len < path.size())
            {
                max_len = path.size();
            }
        }
        System.out.println(max_len + " maximum path length");
        return paths;
    }

    public void remove_tunnel(ArrayList<MPLSPathUnit> tunnel)
    {
        for(MPLSPathUnit mpu : tunnel)
        {
            Device d = (Device) boxes.get(mpu.device_name);
            d.mpls_table.swap_table_bdd.remove(mpu.in_label);
        }
    }

    /**
     * @param path_info: switch, label, switch, label, ..., destination switch of tunneled packets
     */
    public void add_mpls_path(String [] path_info)
    {
        int len = path_info.length;
        String dest_switch = path_info[len-1];
        ForwardingRule fec = new ForwardingRule(((Device)boxes.get(dest_switch)).get_mpls_fec(), 32, null);
        //System.out.println("tunnled pkts: " + fec);

        String ingress = path_info[0];
        HashSet<String> ports = new HashSet<String>();
        String connected_port = get_connected_port(ingress, path_info[2]);
        ports.add(connected_port);
        ((Device) boxes.get(ingress)).add_mpls_encapsulation_entry(fec, Integer.parseInt(path_info[1]), ports);
        System.out.println(ingress + "," + path_info[2] + "," + connected_port);
        for(int i = 2; i < len-2; i = i + 2)
        {
            ports = new HashSet<String> ();
            //System.out.println(path_info[i+2]);
            connected_port = get_connected_port(path_info[i], path_info[i+2]);
            ports.add(connected_port);

            ((Device) boxes.get(path_info[i])).add_mpls_switch_entry(Integer.parseInt(path_info[i-1]), 
                    Integer.parseInt(path_info[i+1]), ports);

            System.out.println(path_info[i] + "," + path_info[i+2] + "," + connected_port);

        }
    }

    /**
     * @param path_info: switch, label, switch, label, ...,  
     * @param fec: tunneled packets
     */
    public void add_mpls_path(String [] path_info, ForwardingRule fec)
    {
        int len = path_info.length;

        String ingress = path_info[0];
        HashSet<String> ports = new HashSet<String>();
        String connected_port = get_connected_port(ingress, path_info[2]);
        ports.add(connected_port);
        ((Device) boxes.get(ingress)).add_mpls_encapsulation_entry(fec, Integer.parseInt(path_info[1]), ports);
        System.out.println(ingress + "," + path_info[2] + "," + connected_port);
        for(int i = 2; i < len-2; i = i + 2)
        {
            ports = new HashSet<String> ();
            //System.out.println(path_info[i+2]);
            connected_port = get_connected_port(path_info[i], path_info[i+2]);
            ports.add(connected_port);

            ((Device) boxes.get(path_info[i])).add_mpls_switch_entry(Integer.parseInt(path_info[i-1]), 
                    Integer.parseInt(path_info[i+1]), ports);

            System.out.println(path_info[i] + "," + path_info[i+2] + "," + connected_port);

        }
    }

    /**
     * for update
     * @param path_info
     */
    public void add_mpls_path_update(String [] path_info)
    {
        int len = path_info.length;
        String dest_switch = path_info[len-1];
        ForwardingRule fec = new ForwardingRule(((Device)boxes.get(dest_switch)).get_mpls_fec(), 32, null);
        //System.out.println("tunnled pkts: " + fec);

        String ingress = path_info[0];
        HashSet<String> ports = new HashSet<String>();
        String connected_port = get_connected_port(ingress, path_info[2]);
        ports.add(connected_port);
        ((Device) boxes.get(ingress)).add_mpls_encapsulation_entry_bdd(fec, Integer.parseInt(path_info[1]), ports);
        System.out.println(ingress + "," + path_info[2] + "," + connected_port);
        for(int i = 2; i < len-2; i = i + 2)
        {
            ports = new HashSet<String> ();
            //System.out.println(path_info[i+2]);
            connected_port = get_connected_port(path_info[i], path_info[i+2]);
            ports.add(connected_port);

            ((Device) boxes.get(path_info[i])).add_mpls_switch_entry_bdd(Integer.parseInt(path_info[i-1]), 
                    Integer.parseInt(path_info[i+1]), ports);

            System.out.println(path_info[i] + "," + path_info[i+2] + "," + connected_port);

        }
    }

    private String get_connected_port(String d1, String d2)
    {
        for(PositionTuple pt : topology.keySet())
        {
            if(pt.getDeviceName().equals(d1))
            {
                for(PositionTuple pt2 : topology.get(pt))
                {
                    if(pt2.getDeviceName().equals(d2))
                    {
                        return pt.getPortName();
                    }
                }
            }
        }

        System.err.println("cannot find port connecting "+ d1+ " to "+d2);
        System.exit(-1);
        return null;
    }

    /**
     * for experiments
     */
    public void add_multiple_transformers()
    {
        String dest_name = "newy32aoa";
        add_nat(dest_name);
        Device dest = (Device) boxes.get(dest_name);

        ForwardingRule fec = new ForwardingRule(dest.nat_addr + dest.nat_subnet_id-1, 32, null);
        add_ipinip_tunnel("seat", "atla", fec);

        String[] mpls_tunnel = new String[]{"losa", "1000", "hous", "3", "kans"};
        add_mpls_path(mpls_tunnel, fec);

    }

    public void add_ipinip_tunnel(String entry, String exit, String destination)
    {
        Device exit_d = (Device) boxes.get(exit);
        Device entry_d = (Device) boxes.get(entry);
        Device destination_d = (Device) boxes.get(destination);

        long exit_addr = exit_d.get_tunnel_exit_addr();
        ForwardingRule fec = new ForwardingRule(destination_d.get_tunnelled_pkt(), 32, null);

        exit_d.add_ipinip_decapsulator(fec, exit_addr);
        entry_d.add_ipinip_encapsulator(fec, exit_addr);

        System.out.println("tunneled pkt " + fec.getdestip());
        System.out.println("exit address " + exit_addr);
    }

    public void add_ipinip_tunnel(String entry, String exit, ForwardingRule fec)
    {
        Device exit_d = (Device) boxes.get(exit);
        Device entry_d = (Device) boxes.get(entry);

        long exit_addr = exit_d.get_tunnel_exit_addr();

        exit_d.add_ipinip_decapsulator(fec, exit_addr);
        entry_d.add_ipinip_encapsulator(fec, exit_addr);

        System.out.println("tunneled pkt " + fec.getdestip());
        System.out.println("exit address " + exit_addr);
    }

    public void add_ipinip_tunnel_update(String entry, String exit, String destination)
    {
        Device exit_d = (Device) boxes.get(exit);
        Device entry_d = (Device) boxes.get(entry);
        Device destination_d = (Device) boxes.get(destination);

        long exit_addr = exit_d.get_tunnel_exit_addr();
        ForwardingRule fec = new ForwardingRule(destination_d.get_tunnelled_pkt(), 32, null);

        exit_d.add_ipinip_decapsulator_update(fec, exit_addr);
        entry_d.add_ipinip_encapsulator_update(fec, exit_addr);

        System.out.println("tunneled pkt " + fec.getdestip());
        System.out.println("exit address " + exit_addr);
    }

    public void ini_mpls()
    {
        for(Box box : boxes.values())
        {
            ((Device) box).ini_mpls_table();
        }
    }

    public void ini_IPinIP ()
    {
        bddengine.createIPinIPPermutation();
        for(Box box : boxes.values())
        {
            ((Device) box).ini_IPinIP();
        }
    }

    public void convert_mpls_bdd()
    {
        for(Box box : boxes.values())
        {
            if(box instanceof Device)
            {
                ((Device) box).mpls_table.convert_to_bdd_table();
            }
        }
    }


    public static void main (String[] args) throws Exception
    {
        //Network n = new Network("i2", true, false);
        //System.out.println("# of active ports:" + n.topology.size());
        //n.extract_mpls_path();

        long t1 = System.currentTimeMillis();
        Network n = new Network("i2", false, false);
        long t2 = System.currentTimeMillis();
        System.out.println("preprocessing time takes " + (t2-t1) + " ms");

    }

}
